(set-logic QF_LIA)
(set-option :model_validate true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i6 Int)
(declare-const i11 Int)
(declare-const v12 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const i14 Int)
(declare-const v27 Bool)
(declare-const v32 Bool)
(assert (or v32 (>= 905 i6) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14)))
(assert (or (= i6 i1) (= i0 150) (>= 905 i6)))
(assert (or v32 (>= 905 i6) v7))
(assert (or (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (=> v8 (not v4))))
(assert (or (not v14) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (= i1 i11)))
(assert (or v7 v32 (< 780 i14)))
(assert (or (not v14) v27 v2))
(assert (or (= i1 i11) v7 (= i0 150)))
(assert (or v32 v7 (not v14)))
(assert (or v7 (>= 905 i6) (=> v8 (not v4))))
(assert (or v15 (= i6 i1) (not v14)))
(assert (or (< 780 i14) (< 780 i14) v27))
(assert (or v2 (not v14) (>= 905 i6)))
(assert (or (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) v32 (= i6 i1)))
(assert (or v32 (< 780 i14) (>= 905 i6)))
(minimize i1)
(check-sat)